\documentclass[times,10pt,twocolumn]{article}
\usepackage{latex8}
\usepackage{times}


%
% PREAMBLE
%
% \usepackage{latexsym}

% include alltt for advanced verbatim
\usepackage{alltt}

% include vdm for mathematical VDM
\usepackage{vdm}

\usepackage{listings}

% language settings - UK spelling
\usepackage[english]{babel}

% graphics includes
\usepackage{graphicx}
\usepackage{epsfig}

% symbol includes
%\usepackage{amssymb}

% Tab for hand-formatting:
\newcommand{\tab}{\hspace*{2em}}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\concat}{\ \hat{}\ }
\newcommand{\duration}{\mbox{\it duration}}
\newcommand{\period}{\mbox{\it periodic}}
%\newcommand{\op}{\mbox{\it op}}
\newcommand{\syn}{\mbox{\it syn?}}
%\newcommand{\call}{\mbox{\it call}}
\newcommand{\send}{\mbox{\it send}}
\newcommand{\thread}{\mbox{\it thread}}
\newcommand{\start}{\mbox{\it start}}
%\newcommand{\return}{\mbox{\it return}}
\newcommand{\await}{\mbox{\it await}}
\newcommand{\deliver}{\mbox{\it deliver}}
\newcommand{\skp}{\mbox{\it skip}}
\newcommand{\node}{\mbox{\it node}}
\newcommand{\instr}{\mbox{\it instr}}
\newcommand{\status}{\mbox{\it status}}
\newcommand{\dormant}{\mbox{\it dormant}}
\newcommand{\alive}{\mbox{\it alive}}
\newcommand{\waiting}{\mbox{\it waiting}}
\newcommand{\linkset}{\mbox{\it linkset}}
\newcommand{\curthr}{\mbox{\it curthr}}
\newcommand{\exec}{\mbox{\it exec}}
\newcommand{\fresh}{\mbox{\it fresh}}
\newcommand{\oid}{\mbox{\it oid}}
\newcommand{\obj}{\mbox{\it obj}}
\newcommand{\now}{\mbox{\it now}}
\newcommand{\head}{\mbox{\it head}}
\newcommand{\tail}{\mbox{\it tail}}
\newcommand{\insrt}{\mbox{\it insert}}
\newcommand{\add}{\mbox{\it add}}
\newcommand{\remove}{\mbox{\it remove}}
\newcommand{\queue}{\mbox{\it queue}}
\newcommand{\sequence}{\mbox{\it seq}}
%\newcommand{\set}{\mbox{\it set}}
\newcommand{\Node}{\mbox{\it Node}}
\newcommand{\Link}{\mbox{\it Link}}
\newcommand{\Thread}{\mbox{\it Thread}}
\newcommand{\Instruction}{\mbox{\it Instruction}}
\newcommand{\ObjectId}{\mbox{\it ObjectId}}
\newcommand{\Operation}{\mbox{\it Operation}}
\newcommand{\Message}{\mbox{\it Message}}
\newcommand{\Time}{\mbox{\it Time}}
\newcommand{\IS}{\mbox{\it IS}}

\newcommand{\Occ}{\mathcal{O}}
\newcommand{\Ex}{\mathcal{E}}

% definition of VDM++, JavaCC, JJTree, JTB, ANTLR and SableCC for listings
\include{customlangdef}
% define the layout for listings
\lstdefinestyle{tool}{basicstyle=\ttfamily,
                         frame=trBL, 
			 showstringspaces=false, 
			 frameround=ffff, 
			 framexleftmargin=0mm, 
			 framexrightmargin=0mm}
\lstdefinestyle{mystyle}{basicstyle=\ttfamily,
                         frame=trBL, 
%                         numbers=left, 
%			 gobble=0, 
			 showstringspaces=false, 
%			 linewidth=\textwidth, 
			 frameround=fttt, 
			 aboveskip=5mm,
			 belowskip=5mm,
			 framexleftmargin=0mm, 
			 framexrightmargin=0mm}
%\lstdefinestyle{mystyle}{basicstyle=\sffamily\small,
%			 frame=tb,
%                         numbers=left,
%			 gobble=0,
%			 showstringspaces=false,
%			 linewidth=345pt,
%			 frameround=ffff,
%			 framexleftmargin=8mm,
%			 framexrightmargin=8mm,
%			 framextopmargin=1mm,
%			 framexbottommargin=1mm,
%			 aboveskip=7mm,
%			 belowskip=5mm,
%			 xleftmargin=10mm,}

\lstset{style=mystyle}
\lstset{language=VDM++}
\lstset{alsolanguage=Java}
% The command below enables you to escape into normal LaTeX mode inside your 
% VDM chunks by starting with a `?� character and ending with a `��
%\lstset{escapeinside=?�}

\newcommand{\vdmtools}{\textsc{VDMTools}\/}
%%\newcommand{\tbw}{\textsc{To Be Written}\/}

%%
%% START OF THE DOCUMENT
%%

\begin{document}

% use empty page style
\pagestyle{empty}

% the title page
\title{Multichannel Audio Filtering using CUDA}

\author{Peter Hoegh Mikkelsen\\
University of Aarhus, Denmark\\phm@iha.dk\\
}


\maketitle
\thispagestyle{empty}

\begin{abstract}
  We present a tool-supported approach to the validation of
  system-level timing properties in formal models of distributed
  real-time embedded systems. Our aim is to provide system architects
  with rapid feedback on the timing characteristics of alternative
  designs in the often volatile early stages of the development cycle.
  The approach extends the Vienna Development Method (VDM++), a formal
  object-oriented modeling language with facilities for describing
  real-time applications deployed over a distributed infra\-structure.
  A new facility is proposed for stating and checking validation
  conjectures (assertions concerning real-time properties) against
  traces derived from the execution of scenarios on VDM++ models. We
  define validation conjectures and outline their semantics. We
  describe the checking of conjectures against execution traces as a
  formally-defined extension of the existing VDM++ tool set, and show
  tools to visualise traces and validation conjecture violations. The
  approach and tool support are illustrated with a case study based on
  an in-car radio navigation system.
\end{abstract}

\section{Introduction}
\label{sec:intro}

% The early stages in the life cycle of computer-based systems are often
% characterized by complexity and volatility of requirements. This is
% particularly true in the development of software to be distributed
% over networked processors in embedded and control applications. In
% this environment, system architects require tools that support a rapid
% and iterative development cycle by providing feedback on models
% embodying design decisions. There is a particular need to assess the
% validity of system-level timing properties. The goal of our current
% work is to support the cost-effective construction and analysis of
% formal models in such a context. 

The development of real-time embedded control systems to high levels
of assurance is a major technical challenge, particularly when
software is to be distributed over networked processors. The early
development phases of such systems are also often characterised by
complexity and volatility of requirements. In this environment,
developers require tools that support the rapid evaluation of
design models against system-level temporal and functional
properties. Such a validation activity helps to identify requirements
and design defects before a commitment is made to a particular design
strategy. In these early development phases, when developer time is at
a premium, the cost effectiveness and ease of use of validation tools
is significant, as well as the level of rigour supplied by the
modeling language and environment. 

Our current work aims to use formal techniques in an accessible and
cost-effective manner to support validation for models of distributed
and embedded real-time systems. The approach is based on the Vienna
Development Method~(VDM), an established formal method which has been
extended to support modeling of concurrent object-oriented
systems~(VDM++~\cite{Fitzgerald&05}) and real-time and distributed
systems~\cite{Verhoef&06b}. In this paper we define new extensions to
the modeling language and tools to permit the expression of
system-level timing properties and support their validation against
timed traces derived from the execution of scenarios on VDM++ models.
The novel features of this work are the language and semantics of
validation conjectures over timed distributed VDM++ models and their
implementation in a proof-of-concept tool. The impact of the work is
primarily on model developers and analysts, enabling explicit
consideration of system-level properties during modeling process.

Section~\ref{sec:language} introduces the current state of VDM++
technology.  The extensions to accommodate checking of system-level
timing properties, called \emph{validation conjectures}, are shown in
Section~\ref{sec:extensions}. These consist of language extensions to
allow the specification of validation
conjectures~(Section~\ref{sec:VCs}) and formally specified tools
extensions to identify conjecture violations in the execution
traces~(Section~\ref{sec:visualisation}).  We interleave the
description of the language and tool extensions with an example based
on a distributed in-car radio navigation system, introduced informally
in the remainder of this section. Finally the approach and further
work are discussed~(Section~\ref{sec:conclusion}).

\subsection{Example: an In-car Radio Navigation System}

Our example, based on an in-car radio navigation system, was introduced
in the context of performance analysis~\cite{Wandeler&06,Hendriks&06}
and also as a case study in the extension of VDM++ to model timing
requirements and distributed architecture~\cite{Verhoef&06b}. The
navigation system consists of several software applications running on
a common distributed hardware platform. The design challenge is to
develop an architecture capable of satisfying the requirements of the
individual applications. In developing such an architecture, the
designer will need feedback on system-level timing properties of 
alternative models.  The model presented here reflects one of the
proposals that was considered during design.  It consists of three
CPUs on an internal communication bus~(Fig.\ref{fig:casestudy}).  

\begin{figure}[!hbt]
\begin{center}
\includegraphics[width=\columnwidth]{casestudy.png}
%\includegraphics[width=\columnwidth]{casestudy.eps}
\caption{Informal overview of the case study}
\label{fig:casestudy}
\vspace{-8mm}
\end{center}
\end{figure}

There are two applications, \textit{ChangeVolume} and
\textit{ProcessTMC}, represented by the upper and lower groups of gray
boxes in Fig.~\ref{fig:casestudy}. Each application consists of three
tasks.  The \textit{ChangeVolume} application increases the radio
volume in response to a user pressing a ``volume up'' key. Within this
application, the task \texttt{HandleKeyPress} takes care of user
interface input handling, \texttt{AdjustVolumeUp} modifies the volume
accordingly and \texttt{UpdateScreen} displays the new volume setting
on the screen.  The \textit{ProcessTMC} application handles Traffic
Message Channel~(TMC) messages. TMC messages arrive at the
\texttt{HandleTMC} task where they are checked and forwarded to the
\texttt{DecodeTMC} task to be translated into human readable text
which is displayed on the screen by the \texttt{UpdateTMC} task. The
environment of the system is modeled by two additional applications
which inject stimuli and observe the system response. The $vBUS$ and
$vCPU0$ are the virtual bus and CPU on which the environment processes
and the environment-system communications take place.

Before embarking on a potentially expensive rigorous development
process, the system architect may wish to explore whether a given
design alternative, such as the one shown above, will respect
important system-level constraints. These constraints may be derived
from requirements of potentially competing applications. We will use
the term \emph{validation conjecture} to mean a property to be checked
against a model and the term \emph{validation} to cover the
checking process. Some examples of validation conjectures for the
in-car navigation example are listed below:
\begin{description}
\item[C1:] A volume change must be reflected
  in the display within $35\,ms$.
% \item[C2:] A TMC must be displayed within
%   $500\,ms$ of receipt.
\item[C2:] The screen should be updated no more than once every $500\,ms$.
\item[C3:] If the volume is to be adjusted
  upward and is not currently at the maximum, the audible change
  should occur within $100\ ms$.
\item[C4:] The volume is only allowed to be
  at the maximum level for at most $10000\,ms$. 
% This conjecture would
%   be used if, for example, the system has a component designed to
%   automatically lower the volume when it stays too high for too long.
\end{description}
Validation conjectures may be inconsistent, possibly pointing to
inconsistencies between applications' requirements. The validation
process should help to identify such issues, and suggest strengthening
or weakening of the conjectures against a specific design model.

\section{VDM++ Technology}
\label{sec:language}
\label{sec:vdm++}

VDM++ is an object-oriented and model-based specification language
based on the Vienna Development Method. It has a formally defined
syntax, static and dynamic semantics which extend those of the ISO
Standard VDM-SL language~\cite{ISOVDM96x}. For a detailed introduction
to VDM++, the reader is referred to current texts~\cite{Fitzgerald&05}
and the VDM Portal~\cite{VDMPortal}.

%\subsection{VDM++ for Timed Distributed Systems}
%\label{sec:vdm++}

VDM++ supports the construction of abstract system models composed of
class specifications, each of which contains definitions of data
types, instance variables and operations. Abstraction in data is provided
through the use of unconstrained types and abstract collections such
as sets, mappings and sequences. Functionality is modeled abstractly
in terms of operations which may be described explicitly, or may be
underspecified, and may even be characterised solely by
postconditions. Data types may be constrained by predicate invariants
and the invocation of operations may be restricted by predicate
preconditions. The language is thus not in general executable, but has
an executable subset. 

Extensions have recently been proposed to VDM++ in order to better
support the description and analysis of real-time embedded and
distributed systems~\cite{Verhoef06,Verhoef&07}. These include
primitives for modeling deployment to a distributed hardware
architecture and support for asynchronous communication. 

\subsection{Example VDM++ model}
\label{sec:examplemodel}

This section contains extracts from the VDM++ model of the in-car
navigation example initially presented in~\cite{Verhoef&06b}. We focus
on the system model rather than the environment model. There are two
independent applications that consist of three tasks each.  Tasks can
be triggered sporadically~(by external stimuli or by receiving
messages from other tasks) or periodically~(checking for available
data on an input source or delivering data to an output). Note that
task activation by external stimuli can be used to model
\textit{interrupt handling}. The interface handling tasks
\verb+HandleKeyPress+ and \verb+HandleTMC+ tasks belong to this
category. The other tasks in our system model are message triggered.

Application tasks are modeled by asynchronous operations in VDM++. For
example, Fig.~\ref{fig:radio} shows the definitions of
\verb+AdjustVolumeUp+ and \verb+HandleTMC+, which are grouped together
in the \textit{Radio} class. The \verb+AdjustVolumeUp+ operation
increases the instance variable representing the volume and then
asynchronously invokes the operation \verb+UpdateScreen+ in the MMI
object. Note the reference to the \verb+RadNavSys+ class, which
represents the system as a whole.
\begin{figure}[!htb]

{\small \begin{alltt}
class \textit{Radio}

values
  public \textit{MAX} : nat = 10
				
instance variables
  public \textit{volume} : nat := 0  

operations
  async public \textit{AdjustVolumeUp}: nat ==> ()
  \textit{AdjustVolumeUp} ( \textit{pno}) ==
    if \textit{volume} <= \textit{MAX} 
    then ( \textit{volume} := \textit{volume} + 1;
           \textit{RadNavSys`mmi.UpdateScreen}(1,\textit{pno})
         );
  async public \textit{HandleTMC}: nat ==> ()
  \textit{HandleTMC} (\textit{pno}) ==
      \textit{RadNavSys`navigation.DecodeTMC}(\textit{pno});
   ...
end \textit{Radio}
\end{alltt}}
\caption{The \textit{Radio} class}
\label{fig:radio}
%\vspace{-3mm}
\end{figure}


%We use the \emph{skip} statement for illustration
%purposes here, it can be replaced with an arbitrary complex statement to
%describe the actual system function that is performed, for example
%changing the amplifier volume set point.
%Note that \verb+AdjustVolume+ uses the \emph{duration} statement to
%denote that a certain amount of time expires independent of 
%the resource on which it is deployed. The duration statement now states
%that changing the set point always takes 150 time units. For illustration
%purposes, \verb+HandleTMC+ uses the \emph{cycles} statement to denote that
%a certain amount of time expires relative to the capacity of the computation
%resource on which it is deployed. If this operation is deployed on an resource
%that can deliver $1000$ cycles per unit of time then the delay (duration)
%would be 1E5 divided by 1000 is 100 time units. A suitable unit of time
%can be selected by the modeler. 

At the system level, the model must show the allocation of tasks to
computation resources. A special class \texttt{CPU} is provided to
create computation resources; each resource is characterised by its
processing capacity, specified by the number of available cycles per
unit of time and the scheduling policy. Throughout this paper, the
time unit is milliseconds. 
% and a factor to denote the overhead incurred per
%task switch. 
For this case study, fixed priority preemptive scheduling is used,
although our approach is not restricted to any policy in particular. A
special class \texttt{BUS} is provided to create communication
resources, each characterised by its throughput, specified by the
number of messages that can be handled per unit of time and the
scheduling policy that is used to determine the order of the messages
being exchanged.
% and a factor to denote the protocol
%overhead. 
The granularity of a message can be determined by the user.  For
example, it can represent a single byte or a complete Ethernet frame,
whatever is most appropriate for the problem under study. For this
case study, we use First Come First Served scheduling, but again the
approach is not restricted to any policy in particular.  An overview
of the VDM++ system model is presented in Fig.~\ref{fig:system}.

\begin{figure}[!hbt]

{\small
\begin{alltt}
system \textit{RadNavSys}
instance variables
  \textit{-- create the application tasks}
  static public \textit{mmi} := new \textit{MMI}();
  static public \textit{radio} := new \textit{Radio}();
  static public \textit{navigation} := 
                  new \textit{Navigation}();

  \textit{-- create CPU (policy, capacity)}
  \textit{CPU1} : \textit{CPU} := new \textit{CPU}(<FP>, 22E6);
  \textit{CPU2} : \textit{CPU} := new \textit{CPU}(<FP>, 11E6);
  \textit{CPU3} : \textit{CPU} := new \textit{CPU}(<FP>, 113E6);

  \textit{-- create BUS 
  -- (policy, capacity, topology)}
  \textit{BUS1} : \textit{BUS} := new \textit{BUS}(<FCFS>, 72E3, 
                        \{\textit{CPU1}, \textit{CPU2}, \textit{CPU3}\})

operations
  \textit{-- the constructor of the system model}
  public \textit{RadNavSys}: () ==> \textit{RadNavSys}
  \textit{RadNavSys} () ==
     ( \textit{CPU1}.\textit{deploy}(\textit{mmi});         
       \textit{CPU2}.\textit{deploy}(\textit{radio});       
       \textit{CPU3}.\textit{deploy}(\textit{navigation}) ) 
end \textit{RadNavSys}
\end{alltt}}
\caption{System model for the case study}
\label{fig:system}
%\vspace{-4mm}
\end{figure}




\subsection{Tool Support for VDM++}
\label{sec:toolsupport}

VDM++ is supported by an industry-strength tool set, called VDMTools, which
is currently owned and further developed by CSK
Systems~\cite{VDMTools}. VDM++ and VDMTools have been used
successfully in several large-scale industrial
projects~\cite{Berg&99a,Horl&00b,Kurita&05,Fitzgerald&07}. The tools
offer syntax, type and static checking capabilities, code generators,
a pretty printer and an application programmer interface. The main
support for validation is by means of an interpreter allowing the
execution of VDM++ models written within the executable subset of the
language.

An important principle in the development of VDMTools has been that of
`taking one's own medicine'. Most of the components of VDMTools,
including the type checker and interpreter, are specified in VDM and
VDM++. For example, the specification of the interpreter embodies the
operational semantics of the language. When extensions are proposed,
it is necessary to first develop formal specifications for them and
integrate them with the existing specifications before developing the
implementation. This formal approach has proved particularly valuable
in mastering the implementation complexity of some components of the
tool set, and has in turn influenced the development of the language.
We return to this point when we describe tool extensions to support
validation in Section~\ref{sec:visualisation}.

Scenarios defined by the user are essentially test cases consisting of
scripts invoking the model's functionality.  The interpreter executes
the script over the model and returns observable results as well as an
\emph{execution trace} containing, for each internal or bus event, a
time stamp and an indication of the part of the model in which it
appeared. A separate tool (an Eclipse plug-in) called \emph{showtrace}
has been developed for reading execution traces, displaying them
graphically so that the user can readily inspect behaviour after the
execution of a scenario, and thereby gain insight into the ordering
and timing of exchange of messages, activation of threads and
invocation of operations.


\subsection{Example Analysis  of Radio Navigation System Model}
\label{sec:exampletoolsupport}
In order to illustrate how the VDMTools interpreter can be used to
examine different scenarios consider Fig.~\ref{fig:scenario}. This is
a small scenario including two tasks in the environment for changing
the volume and sending a TMC message. The \texttt{VolumeUpKey} and
\texttt{TransmitTMC} objects belong to the environment. Each object is
started and, once the system has responded to their stimuli, various
performance characteristics are evaluated and returned. In addition to
yielding a result, the execution of the scenario produces an execution
trace. Note that our examples here deal with the execution of a single
scenario at a time. Interleaving of scenarios is also possible and can
be defined as a separate test case. 
\begin{figure}[!hbt]

{\small
\begin{alltt}
class \textit{World}
  operations
    public \textit{RunScenario1}: () ==> 
             map seq of char to \textit{perfdata}
    \textit{RunScenario1} () ==
      ( \textit{addEnvironmentTask}("\textit{VolumeUpKey}", 
           new \textit{VolumeUpKey}(10));
        \textit{addEnvironmentTask}("\textit{TransmitTMC}", 
           new \textit{TransmitTMC}(10));
        return \{ \textit{name} |-> 
          \textit{envTasks}(\textit{name}).\textit{getMinMaxAverage}() 
          | \textit{name} in set dom \textit{envTasks} \} );
...
end \textit{World}
\end{alltt}}
\caption{Scenario for Radio Navigation System Model}
\label{fig:scenario}
%\vspace{-4mm}
\end{figure}

% The \emph{showtrace} tool presents the contents of execution traces
% graphically as illustrated in Fig.~\ref{fig:initialtraceview}.  The
% event times shown on the horizontal axis relate to the times at which
% specific events occur.  The execution trace is separated out into
% traces on each of the locales within the architecture. Note that it is
% possible to see both how busy the different components are as well as
% the details for when each thread is swapped in and out in the given
% scenario. 

% \begin{figure}[!hbt]
% \begin{center}
% \includegraphics[width=\columnwidth]{tracescreen.png}
% \caption{Trace View from showtrace}
% \label{fig:initialtraceview}
% \vspace{-8mm}
% \end{center}
% \end{figure}







\section{Extensions to Support Validation}
\label{sec:extensions}

The existing VDM++ and VDMTools framework has been extended so that
explicit logical statements of system-level timing
properties~(validation conjectures) can be checked against execution
traces. Fig.~\ref{fig:traceview} shows the \emph{showtrace} output
resulting from the analysis of the four case study validation
conjectures C1-C4 using the extended framework and the execution
scenario defined in Section~\ref{sec:exampletoolsupport}.

The main window shows a fragment of the execution trace.  The times of
significant events are displayed on the horizontal axis.  Processing
on each architectural unit is shown by coloured horizontal
lines~(colours are used to denote denote thread activities, including
start-up, kill and scheduling). The thin arrows that go to and from
buses indicate message passing whereas the fat arrows going up and
down indicate thread swapping out and in respectively.

The features supporting validation are the list of conjectures at the
bottom of the window and the circular marks on the traces that show
conjecture violations. In Fig.~\ref{fig:traceview}, all the
conjectures have been checked against the execution trace. In the
example, based on the scenario shown above, conjectures \texttt{C1}
and \texttt{C2} are violated and \texttt{C3} and \texttt{C4} have
passed.  The user can select one of the violated validation
conjectures and then the appropriate point in the visualisation is
displayed. In Fig.~\ref{fig:traceview} this is done for conjecture
\texttt{C1}~(see the circles with `\textsf{C1}' next to them).
Here the first \texttt{C1} circle indicates the occurrence of the first
of the events in the given validation conjecture while the second one
indicates the occurrence of the second event violating the constraint
(in this case a deadline that is not met). In order to graphically
visualise the place where a violation takes place it is easy to do so
when it is possible to always relate two event occurrences with each
other and that is the case with the different forms of validation
conjectures that is supported at the moment.

\begin{figure*}%[!hbt]
\begin{center}
%\includegraphics[width=0.65\textwidth]{vcscreen9.eps}
\includegraphics[width=0.65\textwidth]{vcscreen9.png}
\caption{Trace view showing conjecture violations}
\label{fig:traceview}
%\vspace{-8mm}
\end{center}
\end{figure*}

This paper describes how the extended framework is constructed to
support the form of validation illustrated above. The two main
elements of Fig.~\ref{fig:traceview} are the validation conjectures
and the results of their evaluation. Section~\ref{sec:VCs} gives an
informal overview of validation conjectures. The semantics of the
conjectures~(the result of their evaluation over an execution trace)
are embodied in the formal specification of the extended tools,
described in Section~\ref{sec:visualisation}.

\section{Validation Conjectures}
\label{sec:VCs}

Validation conjectures describe the temporal relationships between
system-level events that can be observed in an execution trace. An
execution trace may be thought of as a finite sequence of records, one
for each time unit. We use a discrete abstraction of time by using
natural numbers as time values. Each record contains a set of event
names for the events that occurred at that time, and a snapshot of the
values of the instance variables in the system model at that time.

Events are simply temporal markers; they use up no system resources.
Each event has a unique name and may occur many times in an execution
trace. However, at any one time, there may be at most one occurrence
of a given event. Two kinds of system-level event are detectable in an
execution trace generated from a VDM++ model: \emph{operation events}
and \emph{state transition events}. Operation events occur when
operations are requested, activated, or terminated (denoted
\texttt{\#req(Op)}, \texttt{\#act(Op)} and \texttt{\#fin(Op)}
respectively). State transition events occur when a predicate over the
instance variables of a model becomes true.

Validation conjectures are predicates over execution traces.  We will
write $\Occ(e,i,t)$ to indicate that the $i$th occurrence of event $e$
takes place at time $t$. The variable $i$ ranges over the non-zero
natural numbers $\Nat\sb{1}$, and $t$, representing time, ranges over
the indices of the trace. For example, the simple conjecture
\begin{formula}
  \Occ(\#fin(MMI`UpdateScreen),1,50)
\end{formula}
\noindent
is true in a trace where the first occurrence of the event marking the
termination of the \texttt{UpdateScreen} operation is at exactly time
unit 50. Note that distinct occurrences of an event must happen at
different times and that the occurrence numbers increase incrementally
over time\footnote{The relation $\Occ$ is similar to the occurrence
  relation $\Theta$ in Real-Time Logic~(RTL)\cite{Jahanian&86}, but we
  do not claim here to be using full RTL. The formal definition of
  conjecture evaluation is given in VDM-SL for uniformity with the
  tools framework~(Section~\ref{sec:visualisation}).}.

It is often necessary to check a conjecture that relates to the
specific values of some instance variables. For example, a designer
may wish to check that a variable reaches a certain value at a
specified time. In order to do this conveniently, we introduce the
notion of a \emph{state predicate}. A state predicate is a predicate
over the instance variables of the system model. We will write
$\Ex(p,t)$ to mean that the state predicate $p$ is true of the
variables in the execution trace at time $t$.

In stating a conjecture, it may be necessary to mark the times at
which a predicate becomes true. In order to support this, we introduce
the notion of a \emph{state transition event} which contains a predicate and
which occurs at any time when the predicate becomes true. 

% In the following, we adopt a little
% notation from Real-Time
% Logic~(RTL)\cite{Jahanian&86} to express such
% relationships\footnote{This is not RTL, although we believe that the
%   underlying execution trace model satisfies the monotonicity and
%   transition event axioms of RTL.}. RTL
% extends classical predicate logic by adding an occurrence relation,
% written $\Occ(e,i,t)$, in which $e$ is the name of an event, $i$ is
% its occurrence number and $t$ is the time at which the occurrence
% happens.  The validity of RTL formulae can be assessed over a given
% trace over a discrete time domain and so can represent validation
% conjectures. For example, informally, the formula:
% \begin{formula}
%   \forall{e,i,t}{\Occ(e,i,t) \Implies \Occ(e,i+1,t+20)}
% \end{formula}
% \noindent
% asserts that all occurrences of event $e$ are followed at exactly 20
% time units by the next occurrence of the same event. This particular
% conjecture would of course be false in any finite execution trace
% containing at least one occurrence of $e$ because the final occurrence
% of $e$ would not satisfy the requirement.

% In this paper, a portion of RTL is used in a lightweight
% way to clarify the meanings of the validation conjectures supported by
% the tools developed for VDM++. We do not aim here to give a
% comprehensive treatment of the formal relationship between the
% semantics of timed VDM++ and the semantics of RTL. 
% \fbox{But we should do this in the TR and cite it.}

% \subsubsection*{Validation Conjectures}
% \label{sec:conjectures}

The concepts defined so far are sufficient to construct useful
validation conjectures. In order to allow more efficient detection and
appropriate display of violations, we also identify specific forms or
pattern of conjecture. When such standard forms are used, we can
invoke efficient detection and display functions. In this section, we
introduce three such forms: \emph{separations}, \emph{required
  separations} and \emph{deadlines}.  It should be stressed that these
are not intended to form a comprehensive language of validation
conjectures. However, they illustrate the way in which formal tool
support can be tailored to situations in which such standard formats
are used. 

Intuitively, separation conjectures describe a minimum separation
between specified events, should the events occur.  Required
separations are separations in which the second event is required to
occur at or after the minimum separation.  Deadline conjectures state
that the second event must occur before a deadline is reached after
the occurrence of the first event.  Below, each conjecture pattern and
its semantics are introduced in turn.

A \emph{separation} conjecture is a 5-tuple $Separate(e\sb{1}, c,
e\sb{2}, d, m)$ where $e\sb{1}$ and $e\sb{2}$ are the names of events,
$c$ is a state predicate, $d$ is the minimum acceptable delay between
an occurrence of $e\sb{1}$ and any following occurrence of $e\sb{2}$
provided that $c$ evaluates to true at the occurrence time of
$e\sb{1}$.  If $c$ evaluates to false when $e\sb{1}$ occurs, the
validation conjecture holds independently of the occurrence time of
$e\sb{2}$. The Boolean flag $m$ is called the `match flag', when set to
true, indicates a requirement that the occurrence numbers of $e\sb{1}$
and $e\sb{2}$ should be equal. This allows the designer to record
conjectures that describe some coordination between events. For
example, we may wish to state that a stimulus and response events
occur together in pairs within some time bounds, so the $i$th
occurrence of the stimulus is always followed by the $i$th occurrence
of the response.

A validation conjecture $Separate(e\sb{1},c,e\sb{2},d,m)$
evaluates true over an execution trace if and only if:
\begin{formula}
  \forall{i\sb{1},t\sb{1}}
         {\Occ(e\sb{1},i\sb{1},t\sb{1}) \And \Ex(c,t\sb{1}) \Implies \T1 
          \Not \exists{i\sb{2},t\sb{2}}{\Occ(e\sb{2},i\sb{2},t\sb{2}) \And 
                                               t\sb{1} \leq t\sb{2} < t\sb{1} + d \And \T2 
                                               (m \Implies i\sb{1} = i\sb{2}) \And 
                                               (e\sb{1} = e\sb{2} \Implies i\sb{2} = i\sb{1} +1) }}
\end{formula}
\noindent

We want to allow this and the following expressions to be used for the
specification of conjectures concerning both two occurrences of
different event types ($e1 \neq e2$) and two occurrences of the same
event type ($e1 = e2$). In the latter case, we distinguish the first
and the second instances of the same event type by a requirement to
their occurrence numbers ($e\sb{1} = e\sb{2} \Implies i\sb{2} = i\sb{1}
+1$). The match flag should be used with caution in this case, since
it does not make sense to combine the requirement about matching
occurrence numbers with an expression about two instances of the same
event type.

The \emph{required separation} conjecture is similar to the separation
conjecture but additionally requires that the $e\sb{2}$ event does
occur.  A conjecture $SepRequire(e\sb{1},c,e\sb{2},d,m)$ evaluates to
true over an execution trace if and only if:
\begin{formula}
  \forall{i\sb{1},t\sb{1}}
         {\Occ(e\sb{1},i\sb{1},t\sb{1}) \And \Ex(c,t\sb{1}) \Implies \T1 
          \Not \exists{i\sb{2},t\sb{2}}{\Occ(e\sb{2},i\sb{2},t\sb{2}) \And 
                                               t\sb{1} \leq t\sb{2} < t\sb{1} + d \And \T2 
                                               (m \Implies i\sb{1} = i\sb{2}) \And 
                                               (e\sb{1} = e\sb{2} \Implies i\sb{2} = i\sb{1} +1) } \And \T1
          \exists{i\sb{3},t\sb{3}}{\Occ(e\sb{2},i\sb{3},t\sb{3}) \And 
                                          (m \Implies i\sb{1} = i\sb{3}) \And 
                                          (e\sb{1} = e\sb{2} \Implies i\sb{3} = i\sb{1} +1)}
}
\end{formula}
\noindent
The \emph{Deadline} conjecture places a maximum delay on the
occurrence of the reaction event. Again, the \textit{match} option may
be used to link the occurrence numbers of the stimulus and reaction
events. A validation conjecture $DeadlineMet(e\sb{1},c,e\sb{2},d,m)$
consists of a stimulus event, condition and reaction event; if $c$
holds, $d$ is the maximum tolerable delay between stimulus and
reaction. The conjecture evaluates true over an execution trace if and
only if:
\begin{formula}
  \forall{i\sb{1},t\sb{1}}
         {\Occ(e\sb{1},i\sb{1},t\sb{1}) \And \Ex(c,t\sb{1}) \Implies \T1 
          \exists{i\sb{2},t\sb{2}}{\Occ(e\sb{2},i\sb{2},t\sb{2}) \And 
                                               t\sb{1} \leq t\sb{2} \leq t\sb{1} + d \And \T2 
                                               (m \Implies i\sb{1} = i\sb{2}) \And 
                                               (e\sb{1} = e\sb{2} \Implies i\sb{2} = i\sb{1} +1) } 
}
\end{formula}
\noindent
These basic forms of validation conjecture can be combined. For
example, a conjecture to validate the periodic character of an event
might take the form $Periodic(e,p,j)$ where $e$ is the periodic event,
$p$ is the period and $j$ the allowable jitter. The conjecture might
be defined to be true in a given execution trace if and only if:
\begin{formula}
   DeadlineMet(e,true,e,p+j,false) \And \\
   Separate(e,true,e,p \minus j,false)
\end{formula}
\noindent
evaluates to true over the same trace.

The three forms of conjecture identified above are by no means
exhaustive. For example, one might wish to state that the
non-occurrence of an event in a specified period should trigger the
occurrence of some other event. Expression of non-standard conjectures
will likely entail the use of the basic occurrence relation.
Nevertheless, the approach of defining common forms of conjecture is
extensible and allows for tailored tool support of the kind discussed
in Section~\ref{sec:visualisation}.


\subsection{Example Validation Conjectures}
\label{sec:exampleVCs}

It is possible to use the simple language of validation conjectures to
state system-level timing properties in the case study. In the
following, we give concrete syntax representations for the conjectures
C1-C4 introduced in Section~\ref{sec:intro}. In most cases, the state
predicate component of the conjecture is omitted and treated as
\texttt{true}. In all cases, the match component $m$ is omitted and
defaults to \texttt{false}.

\textbf{C1:} \emph{A volume change must be reflected in the display
  within $35\,ms$.}  In the \verb+Radio+ class, the
\verb+AdjustVolumeUp+ operation invokes the \texttt{UpdateScreen}
operation in the MMI. The conjecture is interpreted formally as a
deadline on the completions of \verb+AdjustVolumeUp+ and the next
screen update \texttt{MMI`UpdateScreen}. This is a weak statement in
that it does not tie the screen update to the specific volume change
event. It could be strengthened by adding operation parameters to the
conjecture to link the stimulus and response.  This can be done using
the formal definitions in Section~\ref{sec:visualisation}.  However,
we omit this for simplicity.
\begin{alltt}
deadlineMet(\#fin(Radio`AdjustVolumeUp),
            \#fin(MMI`UpdateScreen), 35)
\end{alltt}
  

% \item[C2:] \emph{The TMC must be displayed
%     within $500\,ms$ of receipt.} The receipt of the TMC is interpreted as
%   the request on the \texttt{HandleTMC} operation in the Radio.
%
%   \begin{alltt}
%     separate(\#fin(Radio`HandleTMC),
%              \#fin(MMI`UpdateScreen),500)
%   \end{alltt}

\textbf{C2:} \emph{The screen should be updated no more than once
  every $500\,ms$.} This is interpreted as a separation constraint on
the \texttt{MMI`UpdateScreen} screen operation completions.

\begin{alltt}
separate(\#fin(MMI`UpdateScreen),
         \#fin(MMI`UpdateScreen), 500)
\end{alltt} 

As a result of formalising and validating the conjecture, the
architect may observe the inconsistency between C1 and C2 that can
arise if a screen update has to be performed in response to a volume
change at a time less than $500\,ms$ from the last screen update. It
may be appropriate to negotiate a weakening in requirements in such as
case. 


% \emph{Only change the volume
%     (up) if the current volume is not at the maximum level. If the volume
%     is to be adjusted, the audible change should be noticed within a
%     limit of 100 ms.} 

\textbf{C3:} \emph{If the volume is to be adjusted upward and is not
  currently at the maximum, the audible change should occur within
  $100\,ms$.} The current volume is modeled by the value of the
instance variable \texttt{(RadNavSys`radio.volume)}.  The request to
adjust the volume is interpreted as a deadline. The noticing of the
audible change is interpreted as the termination of the
\texttt{Radio`AdjustVolumeUp} operation.

\begin{alltt}
deadlineMet(
  #req(Radio`HandleKeyPress),
  RadNavSys`radio.volume < Radio`MAX,
  #fin(Radio`AdjustVolumeUp), 100)
\end{alltt}

Here again the architect may observe that the formalised conjecture
may be weak by allowing many key presses to be serviced by only one
volume adjustment event. A revised, stronger, conjecture linking
occurrences might be appropriate here. 

\textbf{C4:} \emph{The volume is only allowed to be at the maximum
  level for at most $10000\,ms$. 
% This could be the case if the system was
%   designed to automatically lower the volume after a period of time in
%   order to prevent damages to the audio equipment.
} It is interesting to
note that we do not distinguish between the initiators in controlling
the volume but merely observe the resulting level. The maximum amount
of time in which the volume is allowed to be at the maximum level is
set at $10000\,ms$.

\begin{alltt}
deadlineMet(
  RadNavSys`radio.volume >= Radio`MAX, 
  RadNavSys`radio.volume<Radio`MAX, 
  10000)
\end{alltt}







\section{Extended Tool Support for Validation Conjectures}
\label{sec:visualisation}

The VDMTools interpreter has been extended to record additional data
in the execution trace generated by running a scenario and to use this
to evaluate validation conjectures. A further extension to
\emph{showtrace} allows violations to be identified and explored. In
this section, we describe these extensions, focussing on those
aspects that are relevant to the efficient analysis of the validation
conjecture forms identified in Section~\ref{sec:VCs}.

In accordance with the `taking one's own medicine' principle for
developing VDMTools, we began from the formal specification of the
interpreter before developing the code to implement our extensions.
The interpreter specification is substantial -- over 500 pages of
VDM-SL interleaved with informal explanatory text. Thus, VDM is used
both as the meta-language as well as the source language in the part
described in this section. One additional
module called \texttt{VC} has been added containing the formal
descriptions of data structures and operations for logging execution
trace data and for evaluating validation conjectures.  The \texttt{VC}
module is only 400 lines of VDM-SL and below we will show 
extracts from this. 
%Note that the VDM-SL text in this section is the
%formal description of the interpreter extensions, not VDM++ source
%that the interpreter actually executes.

The intention is that, once a scenario has been executed, it should be
possible to evaluate a set of validation conjectures over the
execution trace. A further extension of the \emph{showtrace} tool
permits the graphical indication of conjecture violations on top of
the visualisation of the simulation of the deployed applications.
This is intended to speed up the error detection and correction cycle
at the abstract design level because the detected violations act as
counter examples that are easy to understand.

The \texttt{VC} module specifies efficient operations that can
determine the validity of a validation conjecture over a given
execution trace. If a violation is detected it will yield a tuple of
information that uniquely identifies for \emph{showtrace} the point at
which the violation takes place. In order to provide for efficient
checking of conjectures, the large execution trace file is not
searched directly. Instead, the trace is represented in an optimised
form. The \texttt{VC} module state has the following
form:

{\small \begin{alltt}
state \textit{VCState} of
  ophistmap : map \textit{AS`Name} to \textit{OpHist}
  instvarhistmap : map \textit{AS`Name} 
                     to \textit{InstVarHist}
end
\end{alltt}}

The state contains a mapping from operation names to operation
histories (\texttt{OpHist}), and from instance variable
names\footnote{The abstract syntax of VDM++ is described in a module
  called \texttt{AS}, in which names of identifiers are denoted by
  the type \texttt{Name}.} to their
histories~(\texttt{InstVarHist}). The \texttt{OpHist} type splits the
execution trace for a given operation into traces of the request,
activation and finish events. Each event trace is a sequence of
records, each containing a timestamp and record of the operation
inputs (for a request event) or result (for a finish event) as well as
a thread identifier. The history of changes made to instance variables
is stored with the actual value assigned to it (a semantic value,
denoted as \texttt{VAL}). Formally:

{\small \begin{alltt}
\textit{OpHist} :: \textit{reqs} : seq of \textit{Req}
          \textit{acts} : seq of \textit{Act}
          \textit{fins} : seq of \textit{Fin};

\textit{Req} :: \textit{tim}   : nat
       \textit{arg}   : [seq of \textit{VAL}]
       \textit{thrid} : nat;

\textit{Act} :: \textit{tim}   : nat
       \textit{thrid} : nat;

\textit{Fin} :: \textit{tim}    : nat
       \textit{result} : [\textit{VAL}]
       \textit{thrid}  : nat;

\textit{InstVarHist} = seq of \textit{InstVar};

\textit{InstVar} :: \textit{tim} : nat
           \textit{val} : VAL
           \textit{thrid} : nat;
\end{alltt}}

All these type definitions include a field called \texttt{thrid} that
is used to keep track of the thread identification of the requesting
thread which is used when the threads and flow of control is presented
visually.

Having separated out the execution trace information in this fashion
one can check for possible violations of a given validation
conjecture.  For example, the operation performing the check for a
violation of a deadline conjecture on the \texttt{VC} module state is
defined as follows:

{\small \begin{alltt}
\textit{EvalDeadlineMet}: \textit{DeadlineMet} ==> 
                 [ nat * \textit{ThreadId} * 
                   [nat] * [\textit{ThreadId}] ]

\textit{EvalDeadlineMet}(
  \textit{mk_DeadlineMet}(\textit{ev1},\textit{p},\textit{ev2},\textit{max},\textit{match})) ==
    if \textit{match}
    then 
      \textit{MatchCheck}(\textit{ev1},\textit{p},\textit{ev2},\textit{max},\textit{<MAX>},false)
    else 
      \textit{AnyCheck}(\textit{ev1},\textit{p},\textit{ev2},\textit{max},\textit{<MAX>},false);
\end{alltt}}

\noindent 
Different checks are made depending upon the \texttt{match} value in
the conjecture.  If no violation is found, the operation yields a
\texttt{nil} value. Otherwise, it returns a tuple indicating the
location of a violation. This tuple contains the time and thread
identifier indicating the first event in the validation conjecture
\texttt{ev1} and also the time and thread identifier of the second
event \texttt{ev2}~(if it does not occur at all the special value
\texttt{nil} is used again). Auxiliary operations extract lists of
events of interest and use these to evaluate whether a violation
occurred. As an example, consider the \texttt{MatchCheck} operation
presented below. This operation performs a check for a violation of a
conjecture in which the \emph{m} flag is true. Thus, we expect 
occurrence numbers of the events linked in the conjecture to be the
same.

{\small \begin{alltt}
\textit{MatchCheck}: \textit{EventExpr} * \textit{Pred} * \textit{EventExpr} *
  nat * \textit{Kind} * bool ==> [nat * \textit{ThreadId} * 
    [nat] * [\textit{ThreadId}]]
\textit{MatchCheck}(\textit{ev1},\textit{pred},\textit{ev2},\textit{delay},\textit{kind},\textit{req}) ==
  let \textit{list1} = \textit{FindList}(\textit{ev1}),
      \textit{list2} = \textit{FindList(ev2)}
  in
    (for \textit{index} = 1 to len \textit{list1} do
      let \textit{t1} = \textit{list1}(\textit{index}).\textit{tim},
          \textit{t2} = if \textit{index} in set inds \textit{list2}
               then \textit{list2}(\textit{index}).\textit{tim} 
               else \textit{<INF>}
      in               
        (if not \textit{PredSatisfied}(\textit{pred},\textit{t1})
         then skip
         elseif \textit{t2} = \textit{<INF>} and \textit{req}
         then return 
                mk_(\textit{t1},\textit{list1}(\textit{index}).\textit{thrid},
                  nil,nil)
         elseif \textit{t2} <> \textit{<INF>} and 
                \textit{Violation}(\textit{t1},\textit{t2},\textit{delay},\textit{kind})
         then return 
                mk_(\textit{t1},\textit{list1}(\textit{index}).\textit{thrid},
                  \textit{t2},\textit{list2}(\textit{index}).\textit{thrid})
        );
     return nil);
\end{alltt}}

Within \texttt{MatchCheck}, the auxiliary operation \texttt{FindList}
extracts the list of a particular event's occurrences, so the 
variable \texttt{index} corresponds to the occurrence number. This
checks all instances of the first event \texttt{ev1} and looks for a
violation in the matching occurrence of \texttt{ev2} (or if no matching
is present whether \texttt{ev2} is required). This operation
illustrates violation checking; the other algorithms are similar in
nature.  The violation information for each validation conjecture is
handed over to the \emph{showtrace} tool for visualisation.

If there were no need for predicates very efficient solvers for
propositional logic could be used. However, we need the possibility
to express the validation conjectures in a simple form. The
checking of predicates is carried out using the \textit{PredSatisfied}
operation. It takes a predicate and the time at which the predicate
needs to be checked. This is defined as follows:

{\small \begin{alltt}
\textit{PredSatisfied}: \textit{Pred} * nat ==> bool
\textit{PredSatisfied}(\textit{pred},\textit{t}) ==
  let mk_\textit{Pred}(\textit{var},\textit{op},\textit{num}) = \textit{pred}
  in
    if \textit{var} in set dom \textit{instvarhistmap}
    then 
      let \textit{hist} = \textit{instvarhistmap}(\textit{var}),
          mk_\textit{InstVar}(\textit{firstt},-,-) = hd \textit{hist}
      in
        if \textit{t} < \textit{firstt}
        then return false
        else (for \textit{i} = 2 to len \textit{hist} do
                if \textit{hist}(\textit{i}-1).\textit{tim} <= \textit{t} and 
                   \textit{t} < \textit{hist}(\textit{i}).\textit{tim}
                then return 
                     \textit{EvalOp}(\textit{hist}(\textit{i}-1).\textit{val},
                            \textit{op},\textit{num});
              return 
              \textit{EvalOp}(\textit{hist}(len \textit{hist}).\textit{val},
                     \textit{op},\textit{num})
             )
   else return false;
\end{alltt}}

The predicate is set to be false if the time requested is
before the instance variable in question has been initialised.
Otherwise it looks through the list of updates that has been made to
the instance variable and evaluates the operator at the time
requested.

% \subsection{Examples of Trace Analysis}
% \label{sec:examplevisualisation}



% \section{Related Work}
% \label{sec:related}


\section{Concluding Remarks}
\label{sec:conclusion}

There is a considerable body of work extending formal model-oriented
specification languages to allow the expression of temporal properties
alongside functionality. Some, in common with VDM++, aim to combine
the expression of temporal behaviour with object-oriented or modular
structuring. Possibly the closest examples are Timed
RSL~\cite{George&98}, combinations of Timed CSP with
Object-Z~\cite{Derrick03} and Timed extensions to B such
as~\cite{Rached&05}. The majority of these works focus on support for
verification of design steps by model checking and proof rather than
validation in early development stages. None of them deal explicitly
with deployment. In the context of UML, the strand of research on
validation of timed system models based on a real-time
profile~\cite{Ober&06,Graf&04} proposes the statement of `duration
constraints' between events by means of observer state machines or
OCL-like expressions. Work on the UniFrame framework~\cite{Liu04}
places a VDM++ model of a distributed real-time system as part of a
chain of formalisms for handling functional and non-functional
properties. The proposed tool chain includes timed trace analysis
based on VDM++ models, although this proposal has not been
implemented.

There has been considerable interest in the analysis of formal models
by animation based on the direct execution of models (rather than a
translated model or execution of code derived from a model). There
have been recent industrial successes. For example,
animation~(extensive testing) of an executable model plays a vital
role in the validation of an embedded integrated circuit for cellular
telephones \cite{Kurita&05}. Liu's work based on the SOFL
language~\cite{Liu&07}, which contains elements derived from VDM, also
supports direct animation of models, in this case from systematically
derived execution scenarios.

The aim of our work has been to support the validation of system-level
temporal properties in an accessible and cost-effective manner.  How
far have we gone towards achieving this?  The approach has a formal
basis, but the goal is pragmatic. Building on an existing modeling
framework in VDM++~\cite{Verhoef&06b}, we have presented a new
semantically well-founded facility for stating and checking
system-level validation conjectures against traces derived from the
execution of models that describe distributed real-time systems.
Tool extensions have been defined formally and have been implemented
to proof-of-concept level.  The outcomes of each trace analysis are
made accessible by using a graphical display and exploiting defined
validation conjecture forms for which specific violation detection and
display features have been defined. Together, these facilities enable
the system architect to adjust the functionality, its deployment, the
architecture or the conjecture itself.

It should be stressed that the validation of execution traces does not
replace formal verification: a failing conjecture is the symptom of a
possible design defect but a passing conjecture is not a proof of
correctness with respect to the real-time constraints. Our objective
here is to provide rapid assessment of the key properties of a design
model, helping to identify deficiencies in requirements and
system-level conjectures in the very early phases of a high assurance
development process.

There are some limitations to the framework as developed so far.
First, although our models are loosely specified, each scenario
execution produces only one execution trace because the implementation
of the operational semantics enforces determinism in order to ensure
reproducibility over multiple traces. Within a single execution, we do
allow non-determinism. Second, the tools do not yet support on-the-fly
evaluation of validation conjectures, although this could readily be
accommodated. Third, we need to widen the range of conjecture forms
for which specialised checking and display tools are available.

There are several other directions in which the proof of concept work
reported here might be extended. Once conjectures have been defined
and have been used to validate the execution of the model (which also
serves as a validation of the conjectures themselves), they can be
used (with event transformation) to validate log files generated by
the final implementation of a system. A further important task is to
begin to evaluate the reliability of the results as an aid to
decision-making among design alternatives. Further, the validation
framework discussed here might be extended to support the evaluation
of fault tolerance strategies at the architectural level. Experiments
combining the interpreter (executing a model of a controller) with a
continuous time simulator suggest that it is possible to model faults
at the interface between the two without clouding the models of either
the controller or the environment process. Finally, we are
investigating the provision of automated proof of validation
conjectures on models in constrained situations. 

The purpose of the work reported here has been to enhance the range of
tools available to designers of distributed embedded real-time systems
in early development stages. The approach is based on the use of
abstract system models that have a formal basis and so can benefit
from rigorous analysis. The priority has been to provide rapid
feedback on the timing properties of abstract system models by
exploiting information gathered during the execution of scenarios. 
This form of validation is not seen as a solitary technique, but can
be used in conjunction with other forms of analysis to support
design-time trade-off and decision-making.

\ 

\noindent 
\textbf{Acknowledgments} The authors wish to thank Jozef Hooman,
Jeremy Bryans, Cliff Jones and the anonymous reviewers for valuable
input on this and previous drafts.  Fitzgerald is grateful to the
European Network on Resilience for Survivability in IST~(ReSIST) and
the EPSRC Platform project on Trustworthy Ambient Systems.

%\IEEEtriggeratref{13}
\raggedright
\bibliographystyle{latex8}

\bibliography{hase}

\end{document}

%
% END DOCUMENT
%
